Report for code.c (Counterexample 3)

1

#include <stdlib.h>  

2

#include <stdio.h>  

3

#include <assert.h>  

4

5

#define LEN 10  

6

7

extern unsigned __VERIFIER_nondet_uint();  

8

extern void __VERIFIER_assume(int);  

9

10

/* EXPLANATION  

11

 * The bug in this code is on line 20,the while loop  

12

 * The line needs to be (low <= high), so that the middle value isn't   

13

 * skipped when low and high converge  

14

 */  

15

16

// Preconditions:   

17

// arr is a sorted array  

18

// size is the size of the array arr   

19

int binary_search_function(int arr[], int size, int target) {  

20

    int low = 0;  

21

    int high = size - 1;  

22

    int mid;  

23

    while (low < high) {  

24

        mid = (low + high)/2;  

25

        if (arr[mid] == target) {  

26

            return mid;  

27

        }  

28

        if (arr[mid] < target) {  

29

            low = mid + 1;  

30

        }  

31

        if (arr[mid] > target) {  

32

            high = mid - 1;  

33

        }  

34

    }  

35

    return -1;  

36

}  

37

38

int dumb_sort(int arr[], int len, int target) {  

39

	for (int i=0; i<len; ++i) {  

40

		if (target == arr[i]) {  

41

			return i;  

42

		}  

43

	}  

44

45

	return -1;  

46

}  

47

48

int main() {  

49

  int arr[LEN] = {   

50

		__VERIFIER_nondet_int(),   

51

		__VERIFIER_nondet_int(),  

52

		__VERIFIER_nondet_int(),  

53

		__VERIFIER_nondet_int(),  

54

    __VERIFIER_nondet_int(),  

55

    __VERIFIER_nondet_int(),  

56

    __VERIFIER_nondet_int(),  

57

    __VERIFIER_nondet_int(),  

58

    __VERIFIER_nondet_int(),  

59

    __VERIFIER_nondet_int(),  

60

  };  

61

62

  int x = __VERIFIER_nondet_int();  

63

64

	for (int i=0; i<LEN-1; ++i) {  

65

		__VERIFIER_assume(arr[i] < arr[i+1]);  

66

	}  

67

68

  int result = binary_search_function(arr, LEN, x);  

69

  printf("Result of binary search is = %d\n", result);  

70

71

  // is the result correct? How can you check?  

72

	if (result != dumb_sort(arr, LEN, x)) {  

73

		assert(0);  

74

	}  

75

76

  return 1;  

77

}  

1

#include <stdlib.h>  

2

#include <stdio.h>  

3

#include <assert.h>  

4

5

#define LEN 10  

6

7

extern unsigned __VERIFIER_nondet_uint();  

8

extern void __VERIFIER_assume(int);  

9

10

/* EXPLANATION  

11

 * The bug in this code is on line 20,the while loop  

12

 * The line needs to be (low <= high), so that the middle value isn't   

13

 * skipped when low and high converge  

14

 */  

15

16

// Preconditions:   

17

// arr is a sorted array  

18

// size is the size of the array arr   

19

int binary_search_function(int arr[], int size, int target) {  

20

    int low = 0;  

21

    int high = size - 1;  

22

    int mid;  

23

    while (low < high) {  

24

        mid = (low + high)/2;  

25

        if (arr[mid] == target) {  

26

            return mid;  

27

        }  

28

        if (arr[mid] < target) {  

29

            low = mid + 1;  

30

        }  

31

        if (arr[mid] > target) {  

32

            high = mid - 1;  

33

        }  

34

    }  

35

    return -1;  

36

}  

37

38

int dumb_sort(int arr[], int len, int target) {  

39

	for (int i=0; i<len; ++i) {  

40

		if (target == arr[i]) {  

41

			return i;  

42

		}  

43

	}  

44

45

	return -1;  

46

}  

47

48

int main() {  

49

  int arr[LEN] = {   

50

		__VERIFIER_nondet_int(),   

51

		__VERIFIER_nondet_int(),  

52

		__VERIFIER_nondet_int(),  

53

		__VERIFIER_nondet_int(),  

54

    __VERIFIER_nondet_int(),  

55

    __VERIFIER_nondet_int(),  

56

    __VERIFIER_nondet_int(),  

57

    __VERIFIER_nondet_int(),  

58

    __VERIFIER_nondet_int(),  

59

    __VERIFIER_nondet_int(),  

60

  };  

61

62

  int x = __VERIFIER_nondet_int();  

63

64

	for (int i=0; i<LEN-1; ++i) {  

65

		__VERIFIER_assume(arr[i] < arr[i+1]);  

66

	}  

67

68

  int result = binary_search_function(arr, LEN, x);  

69

  printf("Result of binary search is = %d\n", result);  

70

71

  // is the result correct? How can you check?  

72

	if (result != dumb_sort(arr, LEN, x)) {  

73

		assert(0);  

74

	}  

75

76

  return 1;  

77

}  

1

/* Macros and inline functions to swap the order of bytes in integer values.  

2

   Copyright (C) 1997-2020 Free Software Foundation, Inc.  

3

   This file is part of the GNU C Library.  

4

5

   The GNU C Library is free software; you can redistribute it and/or  

6

   modify it under the terms of the GNU Lesser General Public  

7

   License as published by the Free Software Foundation; either  

8

   version 2.1 of the License, or (at your option) any later version.  

9

10

   The GNU C Library is distributed in the hope that it will be useful,  

11

   but WITHOUT ANY WARRANTY; without even the implied warranty of  

12

   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  

13

   Lesser General Public License for more details.  

14

15

   You should have received a copy of the GNU Lesser General Public  

16

   License along with the GNU C Library; if not, see  

17

   <https://www.gnu.org/licenses/>.  */  

18

19

#if !defined _BYTESWAP_H && !defined _NETINET_IN_H && !defined _ENDIAN_H  

20

# error "Never use <bits/byteswap.h> directly; include <byteswap.h> instead."  

21

#endif  

22

23

#ifndef _BITS_BYTESWAP_H  

24

#define _BITS_BYTESWAP_H 1  

25

26

#include <features.h>  

27

#include <bits/types.h>  

28

29

/* Swap bytes in 16-bit value.  */  

30

#define __bswap_constant_16(x)					\  

31

  ((__uint16_t) ((((x) >> 8) & 0xff) | (((x) & 0xff) << 8)))  

32

33

static __inline __uint16_t  

34

__bswap_16 (__uint16_t __bsx)  

35

{  

36

#if __GNUC_PREREQ (4, 8)  

37

  return __builtin_bswap16 (__bsx);  

38

#else  

39

  return __bswap_constant_16 (__bsx);  

40

#endif  

41

}  

42

43

/* Swap bytes in 32-bit value.  */  

44

#define __bswap_constant_32(x)					\  

45

  ((((x) & 0xff000000u) >> 24) | (((x) & 0x00ff0000u) >> 8)	\  

46

   | (((x) & 0x0000ff00u) << 8) | (((x) & 0x000000ffu) << 24))  

47

48

static __inline __uint32_t  

49

__bswap_32 (__uint32_t __bsx)  

50

{  

51

#if __GNUC_PREREQ (4, 3)  

52

  return __builtin_bswap32 (__bsx);  

53

#else  

54

  return __bswap_constant_32 (__bsx);  

55

#endif  

56

}  

57

58

/* Swap bytes in 64-bit value.  */  

59

#define __bswap_constant_64(x)			\  

60

  ((((x) & 0xff00000000000000ull) >> 56)	\  

61

   | (((x) & 0x00ff000000000000ull) >> 40)	\  

62

   | (((x) & 0x0000ff0000000000ull) >> 24)	\  

63

   | (((x) & 0x000000ff00000000ull) >> 8)	\  

64

   | (((x) & 0x00000000ff000000ull) << 8)	\  

65

   | (((x) & 0x0000000000ff0000ull) << 24)	\  

66

   | (((x) & 0x000000000000ff00ull) << 40)	\  

67

   | (((x) & 0x00000000000000ffull) << 56))  

68

69

__extension__ static __inline __uint64_t  

70

__bswap_64 (__uint64_t __bsx)  

71

{  

72

#if __GNUC_PREREQ (4, 3)  

73

  return __builtin_bswap64 (__bsx);  

74

#else  

75

  return __bswap_constant_64 (__bsx);  

76

#endif  

77

}  

78

79

#endif /* _BITS_BYTESWAP_H */  

1

/* Inline functions to return unsigned integer values unchanged.  

2

   Copyright (C) 2017-2020 Free Software Foundation, Inc.  

3

   This file is part of the GNU C Library.  

4

5

   The GNU C Library is free software; you can redistribute it and/or  

6

   modify it under the terms of the GNU Lesser General Public  

7

   License as published by the Free Software Foundation; either  

8

   version 2.1 of the License, or (at your option) any later version.  

9

10

   The GNU C Library is distributed in the hope that it will be useful,  

11

   but WITHOUT ANY WARRANTY; without even the implied warranty of  

12

   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  

13

   Lesser General Public License for more details.  

14

15

   You should have received a copy of the GNU Lesser General Public  

16

   License along with the GNU C Library; if not, see  

17

   <https://www.gnu.org/licenses/>.  */  

18

19

#if !defined _NETINET_IN_H && !defined _ENDIAN_H  

20

# error "Never use <bits/uintn-identity.h> directly; include <netinet/in.h> or <endian.h> instead."  

21

#endif  

22

23

#ifndef _BITS_UINTN_IDENTITY_H  

24

#define _BITS_UINTN_IDENTITY_H 1  

25

26

#include <bits/types.h>  

27

28

/* These inline functions are to ensure the appropriate type  

29

   conversions and associated diagnostics from macros that convert to  

30

   a given endianness.  */  

31

32

static __inline __uint16_t  

33

__uint16_identity (__uint16_t __x)  

34

{  

35

  return __x;  

36

}  

37

38

static __inline __uint32_t  

39

__uint32_identity (__uint32_t __x)  

40

{  

41

  return __x;  

42

}  

43

44

static __inline __uint64_t  

45

__uint64_identity (__uint64_t __x)  

46

{  

47

  return __x;  

48

}  

49

50

#endif /* _BITS_UINTN_IDENTITY_H.  */